Nuprl Lemma : idlnk-deq_wf 11,40
idlnk-deq  EqDecider(IdLnk) 
latex

Definitionsid-deq, t  T, Id, x:A. B(x), product-deq(A; B; a; b), x:A  B(x), idlnk-deq, IdLnk
Lemmasproduct-deq wf, Id wf, id-deq wf

origin